Using state variables for the specification and verification of TCSP processes
Identifieur interne : 003051 ( Main/Exploration ); précédent : 003050; suivant : 003052Using state variables for the specification and verification of TCSP processes
Auteurs : M. Alonso [Espagne] ; R. Pe A Mari [Espagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 1993.
Abstract
Abstract: A technique for the specification of TCSP processes based upon the concept of states and state variables is presented. It is shown how safety and liveness properties can be proved for processes specified in this way. Parallel composition of specifications is defined, preserving the failures semantics. A technique related to bisimulations is proposed to prove refinements correct. The technique is extended to handle the concealment of events in the implementing process.
Url:
DOI: 10.1007/3-540-56891-3_43
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002A19
- to stream Istex, to step Curation: 002812
- to stream Istex, to step Checkpoint: 002311
- to stream Main, to step Merge: 003222
- to stream Main, to step Curation: 003051
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Using state variables for the specification and verification of TCSP processes</title><author><name sortKey="Alonso, M" sort="Alonso, M" uniqKey="Alonso M" first="M." last="Alonso">M. Alonso</name></author><author><name sortKey="Pe A Mari, R" sort="Pe A Mari, R" uniqKey="Pe A Mari R" first="R." last="Pe A Mari">R. Pe A Mari</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:225C285053902893F76242874DB7F44FEA8AB99E</idno><date when="1993" year="1993">1993</date><idno type="doi">10.1007/3-540-56891-3_43</idno><idno type="url">https://api.istex.fr/document/225C285053902893F76242874DB7F44FEA8AB99E/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">002A19</idno><idno type="wicri:Area/Istex/Curation">002812</idno><idno type="wicri:Area/Istex/Checkpoint">002311</idno><idno type="wicri:doubleKey">0302-9743:1993:Alonso M:using:state:variables</idno><idno type="wicri:Area/Main/Merge">003222</idno><idno type="wicri:Area/Main/Curation">003051</idno><idno type="wicri:Area/Main/Exploration">003051</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Using state variables for the specification and verification of TCSP processes</title><author><name sortKey="Alonso, M" sort="Alonso, M" uniqKey="Alonso M" first="M." last="Alonso">M. Alonso</name><affiliation wicri:level="1"><country xml:lang="fr">Espagne</country><wicri:regionArea>Departamento de Lenguajes y Sistemas Informáticos, Universidad del Pais Vasco, E-20080, San Sebastian</wicri:regionArea><wicri:noRegion>San Sebastian</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author><author><name sortKey="Pe A Mari, R" sort="Pe A Mari, R" uniqKey="Pe A Mari R" first="R." last="Pe A Mari">R. Pe A Mari</name><affiliation wicri:level="4"><country xml:lang="fr">Espagne</country><wicri:regionArea>Departamento de Informática, Universidad Complutense de Madrid, E-28.040, Madrid</wicri:regionArea><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName><orgName type="university">Université complutense de Madrid</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>1993</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">225C285053902893F76242874DB7F44FEA8AB99E</idno><idno type="DOI">10.1007/3-540-56891-3_43</idno><idno type="ChapterID">43</idno><idno type="ChapterID">Chap43</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: A technique for the specification of TCSP processes based upon the concept of states and state variables is presented. It is shown how safety and liveness properties can be proved for processes specified in this way. Parallel composition of specifications is defined, preserving the failures semantics. A technique related to bisimulations is proposed to prove refinements correct. The technique is extended to handle the concealment of events in the implementing process.</div></front></TEI><affiliations><list><country><li>Espagne</li></country><region><li>Communauté de Madrid</li></region><settlement><li>Madrid</li></settlement><orgName><li>Université complutense de Madrid</li></orgName></list><tree><country name="Espagne"><noRegion><name sortKey="Alonso, M" sort="Alonso, M" uniqKey="Alonso M" first="M." last="Alonso">M. Alonso</name></noRegion><name sortKey="Alonso, M" sort="Alonso, M" uniqKey="Alonso M" first="M." last="Alonso">M. Alonso</name><name sortKey="Pe A Mari, R" sort="Pe A Mari, R" uniqKey="Pe A Mari R" first="R." last="Pe A Mari">R. Pe A Mari</name><name sortKey="Pe A Mari, R" sort="Pe A Mari, R" uniqKey="Pe A Mari R" first="R." last="Pe A Mari">R. Pe A Mari</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Ticri/CIDE/explor/OcrV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003051 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003051 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Ticri/CIDE
|area= OcrV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:225C285053902893F76242874DB7F44FEA8AB99E
|texte= Using state variables for the specification and verification of TCSP processes
}}
| This area was generated with Dilib version V0.6.32. |  |